ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), k:Knd, test:(decl-state(ds)ma-valtype(da; k)).
eclbase(k; test)  ecl(ds; da) 

latex

Definitions	x:A. B(x), t  T, ecl(ds; da), eclbase(k; test), x. t(x), x(s)
Lemmas	ma-valtype wf, bool wf, nat wf, decl-state wf, Knd wf, fpf wf, Id wf